;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "mbmptree.lisp")
(require "icrop.lisp")

(module Mcrop
  (import Ibmptree)
  
  ; Trims the columns outside the new tree dimensions from 
  ; the given row.
  ; pre: oldRow - list of pixels in the current row in
  ;               (col (R G B)) form.
  ;      firstCol - integer equal to the lower bounds for the column
  ;      lastCol - integer equal to the upper bounds for the column
  ; post: a list representing the new row with the pixels
  ;       outside of the column bounds removed
  (defun trim-columns (oldRow firstCol lastCol)
    ; are there more pixels in the old row to add to the new one?
    (if (consp oldRow)
        ; yes, get the next pixel
        (let* ((pixel (car oldRow))
               (col (car pixel)))
          ; is the current pixel's column less than the new
          ; lowest column?
          (if (< col firstCol)
              ; yes, do not add it to the new row and look at the
              ; next pixel
              (trim-columns (cdr oldRow) firstCol lastCol)
              ; no, is the pixel's column greater than the 
              ; max column?
              (if (> col lastCol)
                  ; yes, ignore the rest of the row and return the
                  ; new row
                  nil
                  ; no, add the pixel to the new row, subtract the 
                  ; number of columns deleted from the left side of
                  ; the image from its column number, and look at
                  ; the next pixel
                  (cons (list (- col firstCol) (cadr pixel)
                              (caddr pixel) (cadddr pixel))
                        (trim-columns (cdr oldRow) firstCol 
                                      lastCol)))))
        nil))

  ; Deletes each row in the tree that is outside the new row 
  ; bounds and uses trim-columns to remove all columns that
  ; are outside the new column bounds.
  ; pre: oldTree - the original tree
  ;      newTree - the original tree cropped to the new 
  ;                pixel bounds
  ;      n - integer equal to the current row to examine
  ;      firstRow - integer equal to the number of the first
  ;                 row in the new tree bounds
  ;      firstCol - integer equal to the number of the first
  ;                 column in the new tree bounds
  ;      lastRow - integer equal to the number of the last
  ;                row in the new tree bounds
  ;      lastCol - integer equal to the number of the last
  ;                column in the new tree bounds
  ; post: a new bmp-tree equal to the original tree cropped to 
  ;       the desired pixels.
  (defun crop-helper (oldTree newTree n firstRow firstCol lastRow
                              lastCol)
    ; Is the new tree a bmp-tree, is the current row number a
    ; nonnegative integer, and is the row number less than or
    ; equal to the number of the last row in the new bounds?
    (if (and (bmp-tree? newTree) (natp n) (<= n lastRow))
        ; yes, is the current row number less than that of the
        ; first row in the new bouds?
        (if (< n firstRow)
            ; yes, do not add the current row and move to the 
            ; first row of the cropped bitmap
            (crop-helper oldTree newTree firstRow firstRow firstCol
                         lastRow lastCol)
            ; no, trim any undesired columns off of the current 
            ; row and add it to the new tree
            (let* ((oldRow (get-row oldTree n))
                   (newRow (trim-columns oldRow firstCol lastCol))
                   (tempTree (insert-row newTree 
                                         (- n firstRow) newRow)))
              ; examine the next row
              (crop-helper oldTree tempTree (+ n 1) firstRow
                           firstCol lastRow lastCol)))
        ; no, return the new tree
        newTree))

  ; Constructs a new bmp-tree that is equal to the old tree but
  ; cropped to the specified bounds. The upper bound is the top
  ; left corner of the image and the lower bound is the lower
  ; right corner of the image. It also sets the dimensions
  ; in the header of the new tree to the bounds of the
  ; new image.
  ; pre: tr - original bmp-tree
  ;      firstRow - the y-coordinate of the lower bound
  ;      firstCol - the x-coordinate of the lower bound
  ;      lastRow - the y-coordinate of the upper bound
  ;      lastCol - the x-coordinate of the upper bound
  ; post: a bmp-tree cropped to the given bounds.
  (defun crop (tr firstRow firstCol lastRow lastCol)
    ; Is the tree a bmp-tree? Are the new bounds all nonnegative
    ; integers? Are the lower bounds less than the upper bounds?
    (if (and (bmp-tree? tr) (natp firstRow) (natp lastRow)
             (natp firstCol) (natp lastCol) (<= firstRow lastRow)
             (<= firstCol lastCol))
        ; yes, construct a new tree by cropping the old tree
        ; to the new bounds, copying the header from the old tree
        ; into the cropped tree, and changing the dimensions in
        ; the copy to those of the cropped tree.
        (let* ((newHeader (get-header tr))
               (cropTree (crop-helper tr (empty-bmp-tree) firstRow
                                      firstRow firstCol lastRow
                                      lastCol))
               (dimensions (get-dimensions cropTree)))
          (set-dimensions-header (insert-header cropTree
                                                newHeader)
                                 (car dimensions)
                                 (cdr dimensions)))
        ; no, return the unchanged tree
        tr))

  (export Icrop))
